$\forall$${\it es}$:ES, $v$:$\mathbb{B}$, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$\mathbb{B}$)\} , ${\it e'}$:\{${\it e'}$:E$\mid$ $e$ $\leq$loc ${\it e'}$  \& ($x$ after ${\it e'}$) = $v$\} .
\\[0ex]next event in [$e$,${\it e'}$] after which $x$ =$_{b}$ $v$ $\in$ E